$\vdash$ $\forall$$T$:Type, $a$:$T$, $Q$:($T$$\rightarrow\mathbb{P}$). ($a$ = !$x$:$T$. $Q$($x$)) $\Rightarrow$ ($a$ $\in$ \{!$x$:$T$ $\mid$ $Q$($x$)\})